finite{-}type($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$$n$:$\mathbb{N}$, $f$:(\{0..$n$$^{-}$\}$\rightarrow$$T$). Surj(\{0..$n$$^{-}$\}; $T$; $f$)